Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	a__p(0)	→ 0
2:	a__p(s(X))	→ mark(X)
3:	a__leq(0,Y)	→ true
4:	a__leq(s(X),0)	→ false
5:	a__leq(s(X),s(Y))	→ a__leq(mark(X),mark(Y))
6:	a__if(true,X,Y)	→ mark(X)
7:	a__if(false,X,Y)	→ mark(Y)
8:	a__diff(X,Y)	→ a__if(a__leq(mark(X),mark(Y)),0,s(diff(p(X),Y)))
9:	mark(p(X))	→ a__p(mark(X))
10:	mark(leq(X1,X2))	→ a__leq(mark(X1),mark(X2))
11:	mark(if(X1,X2,X3))	→ a__if(mark(X1),X2,X3)
12:	mark(diff(X1,X2))	→ a__diff(mark(X1),mark(X2))
13:	mark(0)	→ 0
14:	mark(s(X))	→ s(mark(X))
15:	mark(true)	→ true
16:	mark(false)	→ false
17:	a__p(X)	→ p(X)
18:	a__leq(X1,X2)	→ leq(X1,X2)
19:	a__if(X1,X2,X3)	→ if(X1,X2,X3)
20:	a__diff(X1,X2)	→ diff(X1,X2)

There are 21 dependency pairs:


21:	A__P(s(X))	→ MARK(X)
22:	A__LEQ(s(X),s(Y))	→ A__LEQ(mark(X),mark(Y))
23:	A__LEQ(s(X),s(Y))	→ MARK(X)
24:	A__LEQ(s(X),s(Y))	→ MARK(Y)
25:	A__IF(true,X,Y)	→ MARK(X)
26:	A__IF(false,X,Y)	→ MARK(Y)
27:	A__DIFF(X,Y)	→ A__IF(a__leq(mark(X),mark(Y)),0,s(diff(p(X),Y)))
28:	A__DIFF(X,Y)	→ A__LEQ(mark(X),mark(Y))
29:	A__DIFF(X,Y)	→ MARK(X)
30:	A__DIFF(X,Y)	→ MARK(Y)
31:	MARK(p(X))	→ A__P(mark(X))
32:	MARK(p(X))	→ MARK(X)
33:	MARK(leq(X1,X2))	→ A__LEQ(mark(X1),mark(X2))
34:	MARK(leq(X1,X2))	→ MARK(X1)
35:	MARK(leq(X1,X2))	→ MARK(X2)
36:	MARK(if(X1,X2,X3))	→ A__IF(mark(X1),X2,X3)
37:	MARK(if(X1,X2,X3))	→ MARK(X1)
38:	MARK(diff(X1,X2))	→ A__DIFF(mark(X1),mark(X2))
39:	MARK(diff(X1,X2))	→ MARK(X1)
40:	MARK(diff(X1,X2))	→ MARK(X2)
41:	MARK(s(X))	→ MARK(X)

Consider the SCC {21-41}. The constraints could not be solved.

Tyrolean Termination Tool (2.37 seconds) --- May 3, 2006